DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2014.625

Parameterized Communicating Automata: Complementation and Model Checking

Authors: Benedikt Bollig, Paul Gastin, and Akshay Kumar

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract

We study the language-theoretical aspects of parameterized communicating automata (PCAs), in which processes communicate via rendez-vous. A given PCA can be run on any topology of bounded degree such as pipelines, rings, ranked trees, and grids. We show that, under a context bound, which restricts the local behavior of each process, PCAs are effectively complementable. Complementability is considered a key aspect of robust automata models and can, in particular, be exploited for verification. In this paper, we use it to obtain a characterization of context-bounded PCAs in terms of monadic second-order (MSO) logic. As the emptiness problem for context-bounded PCAs is decidable for the classes of pipelines, rings, and trees, their model-checking problem wrt. MSO properties also becomes decidable. While previous work on model checking parameterized systems typically uses temporal logics without next operator, our MSO logic allows one to express several natural next modalities.

Cite as

Benedikt Bollig, Paul Gastin, and Akshay Kumar. Parameterized Communicating Automata: Complementation and Model Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 625-637, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.FSTTCS.2014.625,
  author =	{Bollig, Benedikt and Gastin, Paul and Kumar, Akshay},
  title =	{{Parameterized Communicating Automata: Complementation and Model Checking}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{625--637},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.625},
  URN =		{urn:nbn:de:0030-drops-48761},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.625},
  annote =	{Keywords: parameterized verification, complementation, monadic second-order logic}
}

Search Results

Documents authored by Kumar, Akshay

Parameterized Communicating Automata: Complementation and Model Checking

Abstract

Cite as

Thanks for your feedback!

Could not send message